Search Results

Documents authored by Bauer, Andrej

Document
DOI: 10.4230/DagRep.13.10.1
Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)

Authors: Andrej Bauer, Katja Berčič, Florian Rabe, Nicolas Thiéry, and Jure Taslak

Published in: Dagstuhl Reports, Volume 13, Issue 10 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23401 "Automated mathematics: integrating proofs, algorithms and data". The seminar brought together system developers, library authors, and users from key branches of computer-supported mathematics: formalized mathematics, symbolic computation, and mathematical databases. We addressed issues that were common to all areas of computer-supported mathematics: library management, dependencies and interoperability between software components, quality and correctness assurances, searching for information, and usability by end users. Early on in the week, we formed working groups that worked on specific tasks, as described in this report. Each day was divided into a morning talk session and an afternoon period devoted to working in groups. To keep everyone well-informed, we gathered each day before dinner for an informal "show & tell" session.
Cite as

Andrej Bauer, Katja Berčič, Florian Rabe, Nicolas Thiéry, and Jure Taslak. Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401). In Dagstuhl Reports, Volume 13, Issue 10, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{bauer_et_al:DagRep.13.10.1,
  author =	{Bauer, Andrej and Ber\v{c}i\v{c}, Katja and Rabe, Florian and Thi\'{e}ry, Nicolas and Taslak, Jure},
  title =	{{Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)}},
  pages =	{1--23},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{10},
  editor =	{Bauer, Andrej and Ber\v{c}i\v{c}, Katja and Rabe, Florian and Thi\'{e}ry, Nicolas and Taslak, Jure},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.1},
  URN =		{urn:nbn:de:0030-drops-198319},
  doi =		{10.4230/DagRep.13.10.1},
  annote =	{Keywords: mathematical knowledge management, mathematical software, formalized mathematics, computer algebra, databases of mathematical structures}
}
Document
DOI: 10.4230/DagRep.8.8.130
Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)

Authors: Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi

Published in: Dagstuhl Reports, Volume 8, Issue 8 (2019)

Abstract
Formalized mathematics is mathematical knowledge (definitions, theorems, and proofs) represented in digital form suitable for computer processing. The central goal of this seminar was to identify the theoretical advances and practical improvements needed in the area of formalized mathematics, in order to make it a mature technology, truly useful to a larger community of students and researchers in mathematics. During the seminar, various software systems for formalization were compared, and potential improvements to existing systems were investigated. There have also been discussions on the representation of algebraic structures in formalization systems.
Cite as

Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi. Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). In Dagstuhl Reports, Volume 8, Issue 8, pp. 130-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{bauer_et_al:DagRep.8.8.130,
  author =	{Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia},
  title =	{{Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)}},
  pages =	{130--145},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{8},
  number =	{8},
  editor =	{Bauer, Andrej and Escard\'{o}, Mart{\'\i}n and Lumsdaine, Peter L. and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.8.8.130},
  URN =		{urn:nbn:de:0030-drops-102370},
  doi =		{10.4230/DagRep.8.8.130},
  annote =	{Keywords: formal methods, formalized mathematics, proof assistant, type theory}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2016.5
Design and Implementation of the Andromeda Proof Assistant

Authors: Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments. Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization). The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped lambda-calculus, and by implementing a simple automated system for managing a universe of types.
Cite as

Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and Implementation of the Andromeda Proof Assistant. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 5:1-5:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:LIPIcs.TYPES.2016.5,
  author =	{Bauer, Andrej and Gilbert, Ga\"{e}tan and Haselwarter, Philipp G. and Pretnar, Matija and Stone, Christopher A.},
  title =	{{Design and Implementation of the Andromeda Proof Assistant}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{5:1--5:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.5},
  URN =		{urn:nbn:de:0030-drops-98574},
  doi =		{10.4230/LIPIcs.TYPES.2016.5},
  annote =	{Keywords: type theory, proof assistant, equality reflection, computational effects}
}
Document
DOI: 10.4230/DagRep.6.3.44
From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112)

Authors: Andrej Bauer, Martin Hofmann, Matija Pretnar, and Jeremy Yallop

Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)

Abstract
Dagstuhl Seminar 16112 was devoted to research in algebraic effects and handlers, a chapter in the principles of programming languages which addresses computational effects (such as I/O, state, exceptions, nondeterminism, and many others). The speakers and the working groups covered a range of topics, including comparisons between various control mechanisms (handlers vs. delimited control), implementation of an effect system for OCaml, compilation techniques for algebraic effects and handlers, and implementations of effects in Haskell.
Cite as

Andrej Bauer, Martin Hofmann, Matija Pretnar, and Jeremy Yallop. From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112). In Dagstuhl Reports, Volume 6, Issue 3, pp. 44-58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{bauer_et_al:DagRep.6.3.44,
  author =	{Bauer, Andrej and Hofmann, Martin and Pretnar, Matija and Yallop, Jeremy},
  title =	{{From Theory to Practice of Algebraic Effects and Handlers (Dagstuhl Seminar 16112)}},
  pages =	{44--58},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{3},
  editor =	{Bauer, Andrej and Hofmann, Martin and Pretnar, Matija and Yallop, Jeremy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.3.44},
  URN =		{urn:nbn:de:0030-drops-61489},
  doi =		{10.4230/DagRep.6.3.44},
  annote =	{Keywords: algebraic effects, computational effects, handlers, implementation techniques, programming languages}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.CCA.2009
OASIcs, Volume 11, CCA'09, Complete Volume

Authors: Andrej Bauer, Peter Hertling, and Ker-I Ko

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)

Abstract
OASIcs, Volume 11, CCA'09, Complete Volume
Cite as

6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Proceedings{bauer_et_al:OASIcs.CCA.2009,
  title =	{{OASIcs, Volume 11, CCA'09, Complete Volume}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{11},
  editor =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009},
  URN =		{urn:nbn:de:0030-drops-35738},
  doi =		{10.4230/OASIcs.CCA.2009},
  annote =	{Keywords: Mathematics of Computing, Analysis of Algorithms and Problem Complexity}
}
Document
Front Matter
DOI: 10.4230/OASIcs.CCA.2009.2248
CCA 2009 Front Matter - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis

Authors: Andrej Bauer, Peter Hertling, and Ker-I Ko

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)

Abstract
The Sixth International Conference on Computability and Complexity in Analysis, CCA 2009, took place on August 18 to 22, 2009, in Ljubljana, Slovenia. The conference is concerned with Computable Analysis, the theory of computability and complexity over real-valued data. The conference program consisted of 4 invited talks, 2 tutorials of three talks each, and 24 contributed talks. These proceedings contain the abstracts or extended abstracts of the invited talks, tutorials, and a selection of 22 contributed articles.
Cite as

6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. i-ii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:OASIcs.CCA.2009.2248,
  author =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  title =	{{CCA 2009 Front Matter - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  pages =	{i--ii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2248},
  URN =		{urn:nbn:de:0030-drops-22486},
  doi =		{10.4230/OASIcs.CCA.2009.2248},
  annote =	{Keywords: Computable analysis, computability, complexity, Turing machine, constructive mathematics, real number computation, computer arithmetic, exact real ari}
}
Document
DOI: 10.4230/OASIcs.CCA.2009.2249
CCA 2009 Preface - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis

Authors: Andrej Bauer, Peter Hertling, and Ker-I Ko

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)

Abstract
The Sixth International Conference on Computability and Complexity in Analysis, CCA 2009, took place on August 18 to 22, 2009, in Ljubljana, Slovenia. The conference is concerned with Computable Analysis, the theory of computability and complexity over real-valued data. The conference program consisted of 4 invited talks, 2 tutorials of three talks each, and 24 contributed talks. These proceedings contain the abstracts or extended abstracts of the invited talks, tutorials, and a selection of 22 contributed articles.
Cite as

Andrej Bauer, Peter Hertling, and Ker-I Ko. CCA 2009 Preface - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis. In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:OASIcs.CCA.2009.2249,
  author =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  title =	{{CCA 2009 Preface - Proceedings of the Sixth International Conference on Computability and Complexity in Analysis}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  pages =	{1--1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2249},
  URN =		{urn:nbn:de:0030-drops-22492},
  doi =		{10.4230/OASIcs.CCA.2009.2249},
  annote =	{Keywords: Computable analysis, computability, complexity, Turing machine, constructive mathematics, real number computation, computer arithmetic, exact real ari}
}
Document
DOI: 10.4230/OASIcs.CCA.2009.2257
Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions

Authors: Andrej Bauer and Jens Blanck

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)

Abstract
We prove general theorems about unique existence of effective subalgebras of classical algebras. The theorems are consequences of standard facts about completions of metric spaces within the framework of constructive mathematics, suitably interpreted in realizability models. We work with general realizability models rather than with a particular model of computation. Consequently, all the results are applicable in various established schools of computability, such as type 1 and type 2 effectivity, domain representations, equilogical spaces, and others.
Cite as

Andrej Bauer and Jens Blanck. Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions. In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. 37-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:OASIcs.CCA.2009.2257,
  author =	{Bauer, Andrej and Blanck, Jens},
  title =	{{Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  pages =	{37--48},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2257},
  URN =		{urn:nbn:de:0030-drops-22579},
  doi =		{10.4230/OASIcs.CCA.2009.2257},
  annote =	{Keywords: Effective algebras, realizability, constructive metric spaces}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact